package arlab.formulae

/**
 * Created by IntelliJ IDEA.
 * User: Eve
 * Date: 23.02.12
 * Time: 12:18
 * To change this template use File | Settings | File Templates.
 */

// Terme sind Variablen oder Funktionen
trait Term{
  //gibt eine Liste zurück die Alle Funktionen mitsammt ihren Stelligkeiten zurückgibt.
  def functions: Set[(String,Int)] = Set()
  
  //substituiert alle Variablen aus der uebergebenen map  
  def subst(sfn: Map[Variable, Term]): Term = this
  
  def free :Set[Variable] = freeHelp(Set():Set[Variable])
  def freeHelp(bound:Set[Variable]):Set[Variable]
  def bound:Set[Variable] =Set()
  
}


// eine Variable besteht nur aus einem Namen
case class Variable(name:String) extends Term{

  override  def toString()= name
  override def free()= Set(this)
  
  //gibt eine Liste zurück die Alle Funktionen mitsammt ihren Stelligkeiten zurückgibt.
  override def functions: Set[(String,Int)] = Set((name, 0))

  //Hilfsfunktion für die Bestimmung der freien Variablen
  override def freeHelp(bound:Set[Variable]):Set[Variable]={
     if (bound(this)){
        Set()
     }else{
        Set(this)
     }
  }
  
 
  //substituiert alle Variablen aus der uebergebenen map  
  override def subst(sfn: Map[Variable, Term]): Term = sfn.get(this) match {
        case Some(term) => term
        case None => this  
  }
  

  def variant(vars: Set[Variable]): Variable =
     if (vars(this)){
        Variable(name + "'").variant(vars)
     }else{
        this
     }
     
  def variant2(vars: Set[Term]): Variable =
   {
     if (vars(this)){
        Variable(name + "'").variant2(vars)
     }else{
        this
     }
  }
}

// eine Funktion besitzt einen Namen und eine Anzahl mehrerer verschiedener Terme
case class Function(name:String, terms: Term*) extends Term{
 
 
  // überschreibt die toString-Methode für Funktionen
  override  def toString()=
    name + "(" + terms.mkString(",") + ")"
  //Hilfsfunktion für die Bestimmung der freien Variablen
  override def freeHelp(bound:Set[Variable]):Set[Variable] =
   terms.foldLeft(Set():Set[Variable]){(total,n)=> total ++ n.freeHelp(bound)}



  //gibt eine Liste zurück die Alle Funktionen mitsammt ihren Stelligkeiten zurückgibt.
  override def functions: Set[(String,Int)] = terms.foldLeft(Set((name, terms.length))) {(total, n) => total ++ n.functions}

   
  //substituiert alle Variablen aus der uebergebenen map  
  override def subst(sfn: Map[Variable, Term]): Term =
     Function(name, terms.map(_.subst(sfn)):_*)
  
}


